Nuprl Lemma : es-after-pred
0,22
postcript
pdf
es
:ES,
x
:Id,
e
:E.
first(
e
)
(
x
after pred(
e
)) = (
x
when
e
)
vartype(loc(
e
);
x
)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
P
Q
,
Id
,
E
,
first(
e
)
,
b
,
A
,
vartype(
i
;
x
)
,
P
&
Q
,
ES
Lemmas
event
system
wf
,
es-axioms
,
not
wf
,
assert
wf
,
es-first
wf
,
es-E
wf
,
Id
wf
origin
es:ES, x:Id, e:E. 
first(e) 
(x after pred(e)) = (x when e) 
vartype(loc(e);x) es:ES, x:Id, e:E. first(e) (x after pred(e)) = (x when e) vartype(loc(e);x) Tx:A. B(x) Q
bA